<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
 "http://www.w3.org/TR/html4/loose.dtd">
<!--
  Uses "almost standards mode", standard except for some table cell sizing.
  -->
<html>
<head>
  <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  <title>ProofToys - numbers</title>
  <link id=styles type="text/css" rel="stylesheet" href="logic.css">
  <script src="boilerplate.js"></script>

<style type="text/css">
/* CSS here */
</style>

</head>
<body>

<h1>Prooftoys</h1>

<div id=slogans>
<!-- slogans here -->
</div>

<span id=leftNav>
<!-- Boilerplate HTML goes here -->
</span>

<span id=content>
<h2>Working with real numbers</h2>
<p>
Prooftoys currently has primitive support for working with real
numbers using addition, subtraction, multiplication, and division,
with axioms and basic rules of inference.
<p>
<b>Axioms.</b>
The axioms refer only to addition, multiplication, negation
(<s>neg</s>), and reciprocal (<s>recip</s>).  Subtraction
and division are defined in terms of negation and reciprocal.
<p>
In addition there are axioms stating that the result of the basic
operations on real numbers give real numbers as a result (except for
the reciprocal of zero), though they are not shown here.
<p>
<div id=axiomList></div>
<p>
The first axiom, commutativity of addition
(<code>axiomCommutativePlus</code>), shown as
<s>x + y = y + x</s>, means "for all <i>real numbers</i>
<s>x</s> and <s>y</s>, <s>x + y = y + x</s>.
Since Prooftoys can work with other kinds of values, the full
statements of the axioms say explicitly that they are only guaranteed
for real numbers.  In this case the full statement is:
<s>R x & R y ==> x + y = y + x</s>, or with parentheses to clarify
grouping, <s>((R x) & (R y)) ==> (x + y = y + x)</s>.
<p>
<s>R x</s> means "<s>x</s> is a real number".
The conditions about real numbers are not normally shown in the
Prooftoys displays, to help reduce visual clutter.  The symbols
<s>&</s> and <s>==></s> represent the mathematical
"and" and "implies" relationships, explained further in the
<a href="booleans.html">Logic through Pictures</a> page.
<p>
<b>Doing arithmetic.</b>
The <code>axiomArithmetic</code> axiom schema evaluates basic
arithmetic expressions with numeric arguments.  It works with the
operations <s>+, -, *, /, neg, =, !=, >, >=, &lt;, &le;</s>, and the
predicate <code>R</code> when given numeric literals as arguments.
(When dividing, it accepts only inputs that give exact integer
results.)
<p>
<b>Numeric constants.</b>
Prooftoys supports (integer) real number constants in the usual
syntax, e.g. <code>(x - 2)</code>.  Be sure when subtracting a numeric
constant as in the example to leave a space between the
<code>-</code> and the number, otherwise the parser will the
<code>-</code> as part of the number <code>-2</code> and
<code>x</code> as a function applied to <code>-2</code>.
<p>
<b>With the proof builder.</b>
In the interactive proof builder, find axioms by pressing the
<code>x</code> key on your keyboard without selecting any existing
proof step.  They are under the letter <code>x</code> to reduce
clutter in the initial display of available theorems and rules of
inference.
<p>
<b>Subtraction and division.</b>
The operators <code>-</code> and <code>/</code> are defined, but there
are no rules of inference for them, so it is more convenient to expand
their definitions where they occur.  You can expand the definitions by
selecting an expression that uses them, such as <s>(y - 2)</s> or
<s>(x / z)</s> and requesting the <code>apply</code> rule.
<p>  
<b>Rules of inference.</b> Based on the axioms are a set of simple
rules of inference for real numbers.  You can select an expression in
a proof step and apply one of these to it, associating <code>+</code>
or <code>*</code> to the left or to the right, commuting the
arguments, applying the distributive law or using it in reverse to
group common factors (<code>associatePlusToLeft</code>,
<code>associatePlusToRight</code>, <code>associateTimesToLeft</code>,
<code>associateTimesToRight</code>, <code>distribute</code>, and
<code>group</code>).
<p>
There are also rules related to 1, 0, negation and reciprocal:
<code>plusZeroElim</code>, <code>plusZeroIntro</code>,
<code>timesOneElim</code>, <code>timesOneIntro</code>,
<code>plusNegElim</code>, <code>timesRecipElim</code>, and
<code>timesZeroElim</code>.
<p>
Some of the steps in the example use the Prooftoys "replace" rule.
With this rule one or more occurrences of an expression can be
replaced by one that is equal to it.  If the equation is conditional
(has hypotheses), the resulting statement must satisfy all of its
conditions, so it may be necessary to add them to any existing
hypotheses.

<h3>Worked example</h3>
<p>
This example solves a pair of simple simultaneous equations using the
current Prooftoys axioms and rules of inference.
<p>
Notes: In lines with hypotheses, like
<blockquote>
<s>14. 1, 2: x = 4</s>
</blockquote>
the number 1 is an abbreviation for the assumption introduced on line
1, and the number 2 is an abbreviation for the assumption introduced
on line 2.  So if line 1 assumes <s>x = y * 2</s> and line 2
assumes <s>x + y = 6</s>, the whole line amounts to:
<blockquote>
<s>14. (x = y * 2) & (x + y = 6) ==> x = 4</s>
</blockquote>
<p>
For additional background it may be helpful to read
<a href="booleans.html">Basic logic through pictures</a>
and the <a href="introduction.html">Introduction</a> page.

<div id=sampleProof></div>

</span>

<!-- Storage for state to preserve across page unloads -->
<textarea id=ToyStore rows=20 cols=80 class=hidden></textarea>
<!-- Force some white space to accommodate subproofs. -->
<div style="height: 20em"></div>

<!-- END OF HTML -->

<script>
// Insert boilerplate.
Toy.insertNav();
Toy.insertSlogans();
Toy.mathifyAll();

// On DOM ready:
jQuery(function() {
    var rules = Toy.rules;
    var axiomList = new Toy.ProofControl();
    $('#axiomList').append(axiomList.node);
    window.axiomList = axiomList;
    // Numeric axioms:
    var a1 = rules.axiomCommutativePlus();
    var a2 = rules.axiomAssociativePlus();
    var a3 = rules.axiomCommutativeTimes();
    var a4 = rules.axiomAssociativeTimes();
    var a5 = rules.axiomDistributivity();
    var a6 = rules.axiomPlusZero();
    var a7 = rules.axiomTimesOne();
    var a8 = rules.axiomTimesZero();
    var a9 = rules.axiomNeg();
    var a10 = rules.axiomReciprocal();
    axiomList.setSteps([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10]);

    var sample = new Toy.ProofControl();
    window.sampleProof = sample;
    $('#sampleProof').append(sample.node);
    var step1 = rules.assume('x = y * 2');
    var step2 = rules.assume('x + y = 6');
    var step3 = rules.replace(step1, step2, '/main/left/left');
    var step4 = rules.rewriteWithFact(step3, '/main/left/right',
                                      'a = a * 1');
    var step5 = rules.rewriteWithFact(step4, '/main/left',
                                      'a * b + a * c = a * (b + c)');
    var step6 = rules.arithmetic(step5, '/right/left/right');
    var step7 = rules.divideBoth(step6, Toy.parse('3'));
    var step8 = rules.arithmetic(step7, '/right/right');
    var step9 = rules.apply(step8, '/right/left');
    var step10 = rules.rewriteWithFact(step9, '/right/left',
                                       'a * b * c = a * (b * c)');
    var step11 = rules.rewriteWithFact(step10, '/right/left/right',
                                       'axiomReciprocal');
    var step12 = rules.rewriteWithFact(step11, '/right/left',
                                       'axiomTimesOne');
    var step13 = rules.replace(step12, step1, '/right/right/left');
    var step14 = rules.arithmetic(step13, '/right/right');
    sample.setSteps([step1, step2, step3, step4, step5, step6,
                     step7, step8, step9, step10, step11, step12,
                     step13, step14]);
});

// For debugging.
window.db = Toy.debugString;

</script>
</body>
</html>
